;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "Iformulas-aux.lisp")

(module Mformulas-aux
  
  (defun binary-or (list-of-1s-and-0s)
  (if (consp list-of-1s-and-0s)
      (if (= (car list-of-1s-and-0s) 1)
          1
          (binary-or
           (cdr list-of-1s-and-0s)))
      0))

  (export Iformulas-aux)
)

